*****∧I INDUCTION2;

1 (∀Y.(LIST Y⊃LIST (NILL APP Y))∧∀X.(¬(X=NILL)⊃(LIST X⊃(∀Y.(LIST Y⊃LIST (CDR X APP Y))⊃∀Y.(LIST Y⊃LIST (X APP Y)%
)))))⊃∀X.(LIST X⊃∀Y.(LIST Y⊃LIST (X APP Y)))  

*****∀E APPEND1 NILL,Y;

2 (NILL APP Y)=IF NILL=NILL THEN Y ELSE CONS(CAR NILL,CDR NILL APP Y)  

*****DISTRIB;

3 (NILL APP Y)=IF NILL=NILL THEN Y ELSE CONS(CAR NILL,CDR NILL APP Y)≡IF NILL=NILL THEN (NILL APP Y)=Y ELSE (NIL%
L APP Y)=CONS(CAR NILL,CDR NILL APP Y)  

*****TAUTEQ NILL=NILL ;

4 NILL=NILL  

*****TAUT (NILL APP Y)=Y ↑↑↑:↑;

5 (NILL APP Y)=Y  

*****TAUTEQ LIST Y⊃LIST (NILL APP Y) ↑;

6 LIST Y⊃LIST (NILL APP Y)  

*****LABEL H1;

*****∀I ↑ Y;

7 ∀Y.(LIST Y⊃LIST (NILL APP Y))  

*****∀E APPEND1 X,Y;

8 (X APP Y)=IF X=NILL THEN Y ELSE CONS(CAR X,CDR X APP Y)  

*****DISTRIB;

9 (X APP Y)=IF X=NILL THEN Y ELSE CONS(CAR X,CDR X APP Y)≡IF X=NILL THEN (X APP Y)=Y ELSE (X APP Y)=CONS(CAR X,C%
DR X APP Y)  

*****LABEL NOTXNIL;

*****ASSUME ¬(X=NILL);

10 ¬(X=NILL)  (10)

*****TAUT (X APP Y)=CONS(CAR X,CDR X APP Y) ↑↑↑:NOTXNIL;

11 (X APP Y)=CONS(CAR X,CDR X APP Y)  (10)

*****ASSUME LIST X;

12 LIST X  (12)

*****ASSUME ∀Y.(LIST Y⊃LIST (CDR X APP Y));

13 ∀Y.(LIST Y⊃LIST (CDR X APP Y))  (13)

*****∀E ↑ Y;

14 LIST Y⊃LIST (CDR X APP Y)  (13)

*****∀E CAR X;

15 ¬(X=NILL)⊃(LIST X⊃ELEMENT CAR X)  

*****∀E CONS CAR X,CDR X APP Y;

16 ELEMENT CAR X⊃(LIST (CDR X APP Y)⊃LIST CONS(CAR X,CDR X APP Y))  

*****TAUTEQ LIST Y⊃LIST (X APP Y) NOTXNIL:12,↑↑↑:↑;

17 LIST Y⊃LIST (X APP Y)  (10 12 13)

*****∀I ↑ Y;

18 ∀Y.(LIST Y⊃LIST (X APP Y))  (10 12 13)

*****⊃I 13⊃↑;

19 ∀Y.(LIST Y⊃LIST (CDR X APP Y))⊃∀Y.(LIST Y⊃LIST (X APP Y))  (10 12)

*****⊃I 12⊃↑;

20 LIST X⊃(∀Y.(LIST Y⊃LIST (CDR X APP Y))⊃∀Y.(LIST Y⊃LIST (X APP Y)))  (10)

*****⊃I NOTXNIL⊃↑;

21 ¬(X=NILL)⊃(LIST X⊃(∀Y.(LIST Y⊃LIST (CDR X APP Y))⊃∀Y.(LIST Y⊃LIST (X APP Y))))  

*****∀I ↑ X;

22 ∀X.(¬(X=NILL)⊃(LIST X⊃(∀Y.(LIST Y⊃LIST (CDR X APP Y))⊃∀Y.(LIST Y⊃LIST (X APP Y)))))  

*****TAUT ∀X.(LIST X⊃∀Y.(LIST Y⊃LIST (X APP Y))) 1,H1,↑;

23 ∀X.(LIST X⊃∀Y.(LIST Y⊃LIST (X APP Y)))